#ifndef MONOTONEFRAMEWORK_HPP
#define	MONOTONEFRAMEWORK_HPP

#include <iostream>
#include <iomanip>
#include <list>
#include <vector>
#include <set>
#include <map>
#include "cfg_visitor.hpp"
#include "tree_match.hpp"
#include "Interval.hpp"
#include "set_operations.hpp"
using namespace std;
class CFGvisitorFlatInfo;
class CFGvertex;
class ASTnode;

typedef int label_t;
typedef pair<label_t/*source*/, label_t/*dest*/> edge;

/**
 * L is elements of the lattice
 */
template <typename L>
class MonotoneFramework {
public:
	MonotoneFramework(CFGvisitorFlatInfo *_g);
	virtual L MFP_entry(label_t ell) const = 0;
	virtual L MFP_exit(label_t ell) const = 0;
	void report(string prefix) const 
	{
		int m = 0;
		const int num_labels = this->g->labels.size();
		vector< pair<string,string> > hej;
		hej.reserve(num_labels);
		
		for (int ell = 0; ell < num_labels; ell++) {
			string entry = prefix+"_entry(" + ::stringify(ell) + ") = " + ::stringify(this->MFP_entry(ell));
			string exit = prefix+"_exit(" + ::stringify(ell) + ") = " + ::stringify(this->MFP_exit(ell));

			m = ::max(m, int(entry.size()));
			hej.push_back(make_pair(entry,exit));
		}

		for (int ell = 0; ell < num_labels; ell++) {
			pair<string,string>& p = hej[ell];
			cout << left << setw(m+1) << p.first << " " << p.second << endl;
		}
		cout << endl;
	}

protected:
	void run_worklist();
	virtual list<edge> F() const = 0; // Forward or reverse flow
	virtual set<label_t> E() const = 0; // Extremal labels
	virtual L f_ell(L analysis_ell, label_t ell) const = 0;
	virtual L iota() const = 0; // Iota, initial value
	virtual L bottom() const = 0; // Bottom
	virtual bool square_nsubseteq(L arg1, L arg2) const = 0;
	virtual L square_cup(L arg1, L arg2) const = 0;
	virtual bool is_backwards() const = 0;
	
	CFGvisitorFlatInfo *g; // holds flat information about the graph

	vector<L> analysis; // tempoary analysis result
	list<edge> w; // the worklist
	vector<L> MFP_open;	// Forward:entry. Backward:exit.
	vector<L> MFP_fill; // Forward:exit. Backward:entry.
};

////////////////////////////////////////////////////////////////////////////////

template <typename L>
class ForwardAnalysis : public MonotoneFramework<L> {
public:
	ForwardAnalysis(CFGvisitorFlatInfo *_g) : MonotoneFramework<L>(_g) {}
	L MFP_entry(label_t ell) const {return this->MFP_open[ell];}
	L MFP_exit(label_t ell) const {return this->MFP_fill[ell];}
	list<edge> F() const {return this->g->flow;}
	bool is_backwards() const {return false;}
};

//////////////////////////////////////////////////////////////////////////////////

template <typename L>
class BackwardAnalysis : public MonotoneFramework<L> {
public:
	BackwardAnalysis(CFGvisitorFlatInfo *_g) : MonotoneFramework<L>(_g) {}
	L MFP_entry(label_t ell) const {return this->MFP_fill[ell];}
	L MFP_exit(label_t ell) const {return this->MFP_open[ell];}
	list<edge> F() const {return this->g->flowR;}
	bool is_backwards() const {return true;}
};

////////////////////////////////////////////////////////////////////////////////

typedef pair<string/*var*/, label_t/*label*/> RD_element;
typedef set<RD_element> RD;

class ReachingDefs : public ForwardAnalysis<RD> {
public:
	ReachingDefs(CFGvisitorFlatInfo *_g);	
	void run();

protected:
	set<label_t> E() const;
	RD f_ell(RD analysis_ell, label_t ell) const;
	RD iota() const;
	RD bottom() const;
	bool square_nsubseteq(RD arg1, RD arg2) const;
	RD square_cup(RD arg1, RD arg2) const;
	
private:
	void compute_kill(string name_match, RD& kill) const;
};

////////////////////////////////////////////////////////////////////////////////

typedef string LV_element;	// variable
typedef set<LV_element> LV;	// our set of live-variabels

class LiveVariable : public BackwardAnalysis<LV> {
public:
	LiveVariable(CFGvisitorFlatInfo *_g);	
	void run();
	static pair<LV/*gen*/,LV/*kill*/> compute_kill_gen(CFGvertex *n);

protected:
	set<label_t> E() const;
	LV f_ell(LV analysis_ell, label_t ell) const;
	LV iota() const;
	LV bottom() const;
	bool square_nsubseteq(LV arg1, LV arg2) const;
    LV square_cup(LV arg1, LV arg2) const;

private:
	static LV FV(ASTnode *a);
};


////////////////////////////////////////////////////////////////////////////////

typedef string sign;	// restricted to -1,0,+1
typedef set<sign> signs;
typedef map<string/*var*/, signs> DS;

class DetectionSign : public ForwardAnalysis<DS> {
public:
	DetectionSign(CFGvisitorFlatInfo *_g, ASTnode *_root);	
	void run();
protected:
	set<label_t> E() const;
	DS f_ell(DS analysis_ell, label_t ell) const;
	DS iota() const;
	DS bottom() const;
	bool square_nsubseteq(DS arg1, DS arg2) const;
	DS square_cup(DS arg1, DS arg2) const;
private:
	ASTnode *S_star; // Needed by ASTvisitorFV
	signs getSign(ASTnode *a, DS& sigma) const;
};

////////////////////////////////////////////////////////////////////////////////

class IntervalAnalysis : public ForwardAnalysis<IV> {
public:
	IntervalAnalysis(CFGvisitorFlatInfo *_g, ASTnode *_root);	
	void run();
protected:
	set<label_t> E() const;
	IV f_ell(IV analysis_ell, label_t ell) const;
	IV iota() const;
	IV bottom() const;
	bool square_nsubseteq(IV arg1, IV arg2) const;
	IV square_cup(IV arg1, IV arg2) const;
private:
	ASTnode *S_star; // Needed by ASTvisitorFV
	Interval getInterval(ASTnode *a, IV& sigma) const;
};


#endif	/* MONOTONEFRAMEWORK_HPP */
